the_w:World, e:E. act(e)  {a:Action(loc(e))| (isnull(a))}  

latex

Definitions	x:A. B(x), E, t  T, loc(e), act(e), x. t(x), A, P  Q, False, , x(s)
Lemmas	Id wf, nat wf, not wf, assert wf, w-isnull wf, pi1 wf, w-a wf, pi2 wf, world wf